;; The first four lines of this file were added by Dracula.
;; They tell DrScheme that this is a Dracula Modular ACL2 program.
;; Leave these lines unchanged so that DrScheme can properly load this file.
#reader(planet "reader.rkt" ("cce" "dracula.plt") "modular" "lang")
(interface Ibmptree
  (sig rgb? (colors))
  (sig header? (header))
  (sig get-header (tr))
  (sig bmp-tree? (tr))
  (sig insert-pixel (tr pixel))
  (sig get-pixel-color (tr row column))
  (sig insert-header (tr header))
  (sig get-dimensions (tr))
  (sig set-dimensions-header (tr ht wd)) 
  (sig row-list? (rowlist))
  (sig insert-row (tr row columns))
  (sig get-row (tr row))
  (sig empty-bmp-tree())
  (sig make-bmp-tree (bmplist))
  (sig true-bmp-tree? (tr))
  (sig bmp-flatten (tr))
  (sig make-solid-color-image (height width r g b))
  
  ; contracts
  ; verifies that make-bmp-tree always returns a true bmp-tree
  ; given a legal bmp-list input
  (con make-bmp-tree-returns-true-bmp-tree
       (implies (and (header? (car bmplist))
                     (consp bmplist) (consp (cadr bmplist))
                     (= (len (cadr bmplist)) 3)
                     (natp (caadr bmplist)) (natp (cadadr bmplist))
                     (rgb? (caddadr bmplist))))
       (true-bmp-tree? (make-bmp-tree bmplist)))
  ; verifies the round-trip property for make-bmp-tree and 
  ; bmp-flatten
  (con make-bmp-tree-reverses-bmp-flatten
       (implies (true-bmp-tree? tr))
       (equal tr (make-bmp-tree (bmp-flatten tr))))
  ; verifies that get-header always returns a proper header
  (con get-header-returns-proper-header
       (implies (bmp-tree? tr))
       (header? (get-header tr)))
  ; verifies that insert-header always returns a bmp-tree
  (con insert-header-returns-bmp-tree
       (implies (and (bmp-tree? tr) (header? header)))
       (bmp-tree? (insert-header tr header)))
  ; verifies the round-trip property with insert-header and 
  ; get-header
  (con get-header-on-insert-header-round-trip
       (implies (and (bmp-tree? tr) (header? header)))
       (equal header (get-header (insert-header tr header))))
  ; Verifies that insert-pixel always returns a bmp-tree
  (con insert-pixel-returns-bmp-tree
       (implies (and (bmp-tree? tr) (consp pixel)
                     (natp (car pixel)) (natp (cadr pixel))
                     (rgb? (caddr pixel))))
       (bmp-tree? (insert-pixel tr pixel)))
  ; Verifies the round-trip property with get-pixel-color and
  ; insert-pixel
  (con get-pixel-color-on-insert-pixel-round-trip
       (implies (and (bmp-tree? tr) (consp pixel)
                     (natp (car pixel)) (natp (cadr pixel))
                     (rgb? (caddr pixel))))
       (equal (caddr pixel)
              (get-pixel-color (insert-pixel tr pixel)
                               (car pixel) (cadr pixel))))
  ; verifies that get-pixel-color always returns an RGB list
  (con get-pixel-color-returns-rgb
       (implies (and (bmp-tree? tr) (natp row)
                     (natp column)))
       (rgb? (get-pixel-color tr row column)))
  ; Verifies that get-row always returns a proper row-list
  (con get-row-returns-proper-row-list
       (implies (and (bmp-tree? tr) (natp row)))
       (row-list? (get-row tr row)))
  ; Verifies that insert-row always returns a bmp-tree
  (con insert-row-returns-bmp-tree
       (implies (and (bmp-tree? tr) (natp row) 
                     (row-list? columns)))
       (bmp-tree? (insert-row tr row columns)))
  ; Round-trip property that verifies that insert-row inserts the
  ; given row-list at the correct position in the bmp-tree
  (con get-row-on-insert-row-round-trip
       (implies (and (bmp-tree? tr) (natp row) 
                     (row-list? columns)))
       (equal columns
              (get-row (insert-row tr row columns) row)))
  ; Verifies that get-dimensions always returns a cons pair of 
  ; positive integers
  (con get-dimensions-returns-cons-pair
       (implies (true-bmp-tree? tr))
       (and (consp (get-dimensions tr))
            (= (len (get-dimensions tr)) 2)
            (posp (car (get-dimensions tr)))
            (posp (cdr (get-dimensions tr)))))
  ; Verifies that set-dimensions-header always returns a bmp-tree
  (con set-dimensions-header-returns-bmp-tree
       (implies (and (bmp-tree? tr) (posp ht) (posp wd)))
       (bmp-tree? (set-dimensions-header tr ht wd)))
  )